Section: New Results
Implementation of Bourbaki's Theory of Sets in Coq
Participant : José Grimm.
A paper describing our implementation of the sets of natural numbers, of rational numbers and of real numbers has been published by the Journal of Formalized Reasoning [6].
We implemented Chapter 3, Section 7 (Inverse Limits and Direct Limits) and the start of Chapter 4 (Structures) of the Theory of Sets of Bourbaki, details are found in the Research Report [19]